/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package simhya.modelchecking;

import simhya.model.flat.FlatModel;
import simhya.model.store.Store;
import simhya.model.store.faststore.FastStore;
import simhya.matheval.Expression;
import simhya.matheval.SymbolArray;
import java.util.HashMap;
import java.util.ArrayList;
import simhya.modelchecking.mtl.MTLformula;
import simhya.modelchecking.mtl.parser.MTLlexer;
import simhya.modelchecking.mtl.parser.MTLparser;
import java.io.StringReader;
import java.io.FileReader;
import simhya.modelchecking.parser.SMClexer;
import simhya.modelchecking.parser.SMCparser;

/*
 * TO DO: add command to model check a formula and to run a parameter exploration on one 
 * or more formulas. Use parameterExploration routines. 
 * Add options, like the possibility of model checking the pointwise semantics on ODE 
 * or on CTMC trajectories, and maybe the possibility (?here?) of a quantitative pointwise
 * semantics for ODE.
 * 
 * I need a class for collecting model checking results, supporting also visualization!
 * 
 * 
 */

/**
 *
 * @author Luca
 */
public class SMCenvironment {
    HashMap<String,Expression> predicatesToExpressions;
    ArrayList<MTLformula> MTLformulas;
    HashMap<String,MTLformula> namesToMTLformulas;
    private FlatModel model;
    private Store modelStore;
    private FastStore localStore;
    private int numberOfFormulas;
    private MTLlexer MTLlexer;
    private MTLparser MTLparser;
    private boolean init;
    

    public SMCenvironment(FlatModel model) {
        this.model = model;
        this.modelStore = model.getStore();
        this.reset();
    }
    
    private void reset() {
        this.localStore = new FastStore();
        this.numberOfFormulas = 0;
        this.MTLformulas = new ArrayList<MTLformula>();
        this.predicatesToExpressions = new HashMap<String,Expression>();
        this.namesToMTLformulas = new HashMap<String,MTLformula>();
        this.MTLlexer = null;
        this.MTLparser = null;
        this.init = false;
    }
    
    public void loadEnvironment(String file) {
        if (init)
            reset();
        try {
            FileReader in = new FileReader(file);
            SMClexer lexer = new SMClexer(in);
            SMCparser parser = new SMCparser(lexer,this);
//            parser.debug_parse();
            parser.parse();            
            in.close();
            init = true;
        } catch (Exception e) {
            System.err.println(e.getMessage());
            e.printStackTrace();
            throw new RuntimeException("Cannot load SMC environment " + file);
        }
    }
    
    
    private void initMTLparser(String formula) {
        if (MTLlexer == null || MTLparser == null) {
            MTLlexer = new MTLlexer(new StringReader(formula));
            MTLparser = new MTLparser(MTLlexer);
        } else {
            MTLlexer.yyreset(new StringReader(formula));
        }
    }
    
    /**
     * Adds an MTL formula to the model checking environment with the given name 
     * @param formula
     * @return 
     */
    public boolean addMTLformula(String id, String formula) {
        initMTLparser(formula);
        if (this.namesToMTLformulas.containsKey(id))
            return false;
        try {
            MTLformula f = (MTLformula)(MTLparser.parse().value);
            f.initalize(modelStore, localStore.getParametersReference(), predicatesToExpressions);
            this.namesToMTLformulas.put(id, f);
            this.MTLformulas.add(f);
            this.numberOfFormulas++;
            return true;
        } catch (Exception e) {
            throw new RuntimeException("Cannot parse formula " + id);
        }
    }
    
    /**
     * Adds an MTL formula to the model checking environment with no name 
     * @param formula
     * @return 
     */
    public boolean addMTLformula(String formula) {
        String id = "_formula_" + numberOfFormulas;
        return this.addMTLformula(id, formula);
    }
    
    /**
     * Add a parameter for the model checking environment. 
     * Parameters are stored in a local store.
     * @param name name of the parameter
     * @param definition defining expression
     * @return 
     */
    public boolean addParameter(String name, String definition) {
        if (localStore.getParametersReference().containsSymbol(name))
            return false;
        Expression exp = localStore.parseExpression(definition);
        if (exp.isNumericConstant())
            localStore.addParameter(name, exp.computeValue());
        else
            localStore.addParameter(name, exp.computeValue(), exp);
        return true;
    }
    
    /**
     * Adds an atomic proposition definition to the model checking environment.
     * 
     *
     * @param name
     * @param definition
     * @return 
     */
    public boolean addAtomicProposition(String name, String definition) {
        /*
         * TO DO: allow boolean connectives in the definition of the expression,
         * but only of the form && || !, so that the expression itself can 
         * be parsed by the store. 
         * OR EVEN BETTER: implement a method to define compound atomic predicates in the 
         * file, but keeping track of individual atomic predicates by a special naming convention.
         */
        if (this.predicatesToExpressions.containsKey(name))
            return false;
        Expression exp = modelStore.parseExpression(definition, localStore.getParametersReference());
        exp.setLocalSymbols(localStore.getParametersReference());
        this.predicatesToExpressions.put(name, exp);
        return true;
    }
    
    /*
     * REMEMBER TO RECOMPUTE EXPRESSIONS OF LOCAL PARAMETERS
     */
    
    public void print_debug() {
        System.out.println("****Parameters****");
        for (String s : this.localStore.getParametersReference().getNameOfAllSymbols()) {
            int id = localStore.getParametersReference().getSymbolId(s);
            System.out.println(s + " = " + localStore.getParametersReference().getValue(id));
        }
        System.out.println("\n****Atomic Predicates****");
        for (String s : this.predicatesToExpressions.keySet()) {
            Expression exp = this.predicatesToExpressions.get(s);
            System.out.println(s + " := " + exp.toString());
        }
        System.out.println("\n****MTL Formulae****");
        for (String s : this.namesToMTLformulas.keySet()) {
            MTLformula f = this.namesToMTLformulas.get(s);
            System.out.println(":"+s+":"); 
            System.out.println(f.toFormulaTree());
            System.out.println("****");
        }
    }
    
    /*
     * TO DO: set up options for model checking
     * set up parameter exploration routines
     * 
     */
    
    
    /**
     * Model checks the formula with given name, with parameters and options as previously set
     * @param formulaName
     * @return 
     */
    public SMCoutput modelCheck(String formulaName) {
        MTLformula formula = this.namesToMTLformulas.get(formulaName);
        if (formula == null)
            throw new RuntimeException("SMC: formula " + formulaName + " does not exist");
        return modelCheck(formula);
    } 
    
    /**
     * Model checks the formula with given id, with parameters and options as previously set
     * @param formulaID
     * @return 
     */
    public SMCoutput modelCheck(int formulaID) {
        MTLformula formula = this.MTLformulas.get(formulaID);
        if (formula == null)
            throw new RuntimeException("SMC: formula " + formulaID + " does not exist");
        return modelCheck(formula);
    } 
    
    
    /**
     * Actually does the model checking
     * @param formula
     * @return 
     */
    private SMCoutput modelCheck(MTLformula formula) {
        
        //1. set up the simulator
        
        //2. initialize model checking for formula
        
        //3. simulate until stop condition is true. Possibly add max runs threshold
        
        //4. return the SMCoutput of the formula.
        
        
        return null;
    }
            
    
    
}
